Issue5283.agda:12,5-13
Syntax error: 'tactic' can only appear in attributes
when scope checking tactic ?
